M. Kikuchi, T. Kurahashi, H. Sakai, "On proofs of the incompleteness theorems based on Berry's paradox by Vopěnka, Chaitin, Boolos"
著者
菊池誠
倉橋 太志
酒井 拓史
見れる
https://www.researchgate.net/profile/Taishi-Kurahashi/publication/264380943_On_proofs_of_the_incompleteness_theorems_based_on_Berry's_paradox_by_Vopenka_Chaitin_and_Boolos/links/5a390ff5aca27266cfd34247/On-proofs-of-the-incompleteness-theorems-based-on-Berrys-paradox-by-Vopenka-Chaitin-and-Boolos.pdf?origin=publication_detail
motibavit
Petr Vopěnka，Gregory J. Chaitin，George S. Boolosの新しい不完全性定理の証明について精査する．
Boolos
Berryのパラドックスを用いたGeorge S. Boolosによる不完全性定理の新しい証明
Boolosの不完全性定理と名付けておこう
G. Boolos, "A new proof of the Godel incompleteness theorem"
Abstrakt
By formalizing Berry's paradox, Vopěnka, Chaitin, Boolos and others proved the incompleteness theorems without using the diagonal argument. In this paper, we shall examine these proofs closely and show their relationships.
Firstly, we shall show that we can use the diagonal argument for proofs of the incompleteness theorems based on Berry's paradox. Then, we shall show that an extension of Boolos' proof can be considered as a special case of Chaitin's proof by defining a suitable Kolmogorov complexity. We shall show also that Vopěnka's proof can be reformulated in arithmetic by using the arithmetized completeness theorem.
表記
算術の言語$ \mathscr{L}_\mathrm{A}を固定する．
$ v_0,v_1をconcreteな変数記号として
$ x,yを変数記号全体を動くメタ変数とする．
remark:
不必要に多くの変数記号を用意しない．
すなわち，変数記号$ vは高々有限個とする．
これによって，算術の言語の記号は有限個しか存在しない．
SnO2WMaN.iconここの議論はちょっと理解が怪しい．
$ \mathscr{L}_\mathrm{A}上の算術の標準モデル$ \mathcal{N}を定める．
数項$ \overline{n} \equiv S(S(\cdots S(0)\cdots))とする．
$ \ulcorner \varphi \urcornerは論理式$ \varphiの適当なGödel数とする．
$ |\varphi|は論理式の長さ，すなわち記号列の記号の個数とする．
$ Tは$ \sf PAの再帰的公理化可能な拡大理論とする．
$ \mathrm{Pr}_T(x)は$ Tでの可証性を表した$ \Sigma_1論理式とする．
remark:
本来なら論理式$ \varphiに対して$ \mathrm{Pr}_T \left( \overline{\ulcorner \varphi \urcorner} \right)のようにしなければならない
煩雑になりすぎるので数項であることは省略する．
$ \mathrm{Con}_T \equiv \lnot\mathrm{Pr}_T(\ulcorner 0 = 1 \urcorner)とする．
Lem 2.1: Gödelの不動点補題
任意の論理式$ \varphi\lbrack x,y \rbrackに対し，
以下を満たす，自由変数が$ v_0のみの論理式$ \psi \lbrack v_0 \rbrackが存在する．
$ T \vdash \forall_x. \left\lbrack \psi(x) \leftrightarrow \varphi(x,\ulcorner \psi\lbrack v_0 \rbrack \urcorner) \right\rbrack
Thm 2.2: 導出可能性条件
$ \sigma,\piは任意の文とする．
D1. $ T \vdash \sigma$ \implies$ T \vdash \mathrm{Pr}_T \left(\ulcorner \sigma \urcorner\right)
D2. $ T \vdash \mathrm{Pr}_T \left( \ulcorner \sigma \to \pi \urcorner \right) \to \left( \mathrm{Pr}_T \left( \ulcorner \sigma \urcorner \right) \to \mathrm{Pr}_T \left( \ulcorner \pi \urcorner \right) \right)
D3. $ T \vdash \mathrm{Pr}_T\left( \ulcorner \sigma \urcorner\right) \to \mathrm{Pr}_T\left(\ulcorner\mathrm{Pr}_T\left(\ulcorner\sigma\urcorner\right)\urcorner\right)
Thm 2.3: Σ₁完全性定理，形式化されたΣ₁完全性定理
$ \sigmaは$ \Sigma_1文とする．
Σ₁完全性定理
1. $ \mathcal{N} \vDash \sigma \implies T \vdash \sigma
形式化されたΣ₁完全性定理
2. $ T \vdash \sigma \to \mathrm{Pr}_T(\ulcorner \sigma \urcorner)
remark:
1とMPより，導出可能性条件D1が得られる．
2で$ \sigma \equiv \mathrm{Pr}_T(\pi)とすれば導出可能性条件D3が得られる．
Remark:
Lem 2.1，2.2の2，Thm 2.3の証明は以下を参照．
C. Smoryński, "The incompleteness theorems"
G. Boolos; "The Logic of Provability"
Notation:
停止性に関する表記
$ f,gは(部分)再帰的関数とする．
自然数$ mに対して
$ f(m)が定義されている（止まって，何らかの値を返す）なら$ f(m)\downarrowと表記する．
そうでないなら$ f(m)\uparrowと表記する．
$ f(x) \simeq g(x)と書いたとき，
任意の$ n \in \Nに対して$ f(n) = g(n)か，$ f(n)\uparrowかつ$ g(n)\uparrowであるとする．
2項関係$ R(x,y) \sube \N^2に対し，部分関数$ \mu_y.R(x,y)を
任意の$ m \in \Nに対し，
$ \mu_y.R(m,y)\downarrow$ \iff$ R(m,k)が任意の$ k \leq nで定義されている
$ R(m,k)である中で最小の$ kを$ \mu_y.R(m,y) = kであるとする
remark:$ R(x,y)が再帰的関係なら$ \mu_y.R(x,y)は全域関数である
再帰的全域関数$ (x)_nを，$ xを素因数分解したときの$ n番目の素数の指数部分を指すとする．
example:$ 1440 = 2^5 \times 3^2 \times 5^1より$ (1440)_2 = 2である．
pair関数$ \lang \cdot, \cdot \rang \colon \N^2 \to \Nは再帰的関数であるとする．
また，unpair関数$ \lbrack x\rbrack_iも再帰的関数とする．
$ x = \lang y_0,y_1 \rangであったとき$ \lbrack x\rbrack_i = y_iとする．
すなわち，$ \lbrack \lang y_0,y_1 \rang \rbrack_i = y_iである．
Def.表現可能性
$ \N上の関数$ fが$ Tで表現可能であるとは，次のような$ \varphi(x,y)が存在し，任意の$ m,n \in \Nに対し
$ f(m) = n \iff T \vdash \varphi(\overline{m},\overline{n}) \land \forall_{v_0,v_1}\lbrack \varphi(\overline{m},v_0) \land \varphi(\overline{m},v_1) \to v_0 = v_1 \rbrack
とする．
Prop 2.4: 再帰的関数 = 表現可能
$ \N上の関数について，
$ fが再帰的関数であることと$ Tで表現可能であることは同値である．
proof:
表現可能性定理についてのメモ
Richard Kaye. "Models of Peano arithmetic"参照
Def 2.5: Boolosのnames
$ n \in \Nとし，$ \varphi\lbrack v_0 \rbrackについて
$ \mathcal{N} \models \varphi(\overline{n}) \land \forall_{v_0,v_1}.\lbrack \varphi(v_0) \land \varphi(v_1) \to v_0 = v_1 \rbrackであるとき，$ \varphi(v_0)が$ nを名乗る(names)という．
remark:
直感的にはこの論理式は，真になるなら代入された数は絶対に$ nであるということを主張している．
このnamesの概念を用いてGeorge S. BoolosはBerryのパラドックスを形式化した．
remark:
任意の自然数には，その数を名乗るいくつかの論理式が存在する．
が，それぞれの論理式は高々一つの数しか名乗れない．
Thm 2.6: Boolosの不完全性定理
算術的に真な文だけを計算するアルゴリズムは存在しない．
remark:
Kenneth Jon Barwiseによると見たことのある中では最も直感的なGödelの不完全性定理の証明！と絶賛されている
前原昭二によると意味論（すなわち真という概念）に足を突っ込んでいてもはやGödelの不完全性定理とは言えないのではみたいな批判もある．
オリジナルのGödelの不完全性定理は統語論的な定理であるので．
このあたりは菊池誠; "不完全性定理"も参照．
Remark
標準的な方法では，Boolosの不完全性定理から第2不完全性定理を得ることは出来ない．ということがわかっている
Kikuchi M., "A note on Boolos' proof of the incompleteness theorem"(以下Kikuchi1994と略す．)ではモデル論的証明を行って第2不完全性定理を証明していたとされる．
Def 3.1: Kikuchiのnames
$ n \in \Nとし，$ \varphi\lbrack v_0 \rbrackについて
$ T \vdash \varphi(\overline{n}) \land \forall_{v_0,v_1}.\lbrack \varphi(v_0) \land \varphi(v_1) \to v_0 = v_1 \rbrackであるとき，$ \varphi(v_0)が$ nを名乗る(names)という．
remark:
Boolosのものは$ \mathcal{N} \vDash，一方こっちは$ T \vdashであることに注意！
Remark:
Kikuchi1994では3.1の定義を用いて，対角化補題を用いずにBerryのパラドックスを形式化することで第1不完全性定理を証明し，モデル理論的な手法を用いて第2不完全性定理を証明した．
今回は
Kikuchi1994における証明の独立性は対角線補題を用いても得られること，
モデル理論的な方法を用いずに第2不完全性定理が得られる
ことを証明する．
Berryのパラドックスの形式化に置いて対角線補題と似たようなものが得られることに注目する．
Lem 3.2: 長さに依る対角線補題
任意の論理式$ \varphi\lbrack x,y \rbrackに対し，
以下を満たす，自由変数が$ v_0のみの論理式$ \psi \lbrack v_0 \rbrackが存在する．
$ T \vdash \forall_x. \left\lbrack \psi(x) \leftrightarrow \varphi(x,| \psi\lbrack v_0 \rbrack |) \right\rbrack
proof:
1. $ y = |E_x|を表す再帰的関係?を表現する$ \mathrm{lh}(x,y)が構成出来る．
関数と書いてあるけど関係では？
2. $ \exists_z.\lbrack \varphi(x,z) \land \mathrm{lh}(\ulcorner \psi\lbrack v_0 \rbrack \urcorner, z) \rbrackとしてGödelの不動点補題を適用する．
すなわち，次を満たす$ \psi\lbrack v_0 \rbrackが構成できる．
$ T \vdash \forall_x. \left\lbrack \psi(x) \leftrightarrow \exists_z.\lbrack \varphi(x,z) \land \mathrm{lh}(\ulcorner \psi\lbrack v_0 \rbrack \urcorner, z) \rbrack \right\rbrack
3. $ T \vdash \forall_x.\lbrack \varphi(x,|\psi\lbrack v_0 \rbrack|) \leftrightarrow \exists_z.\lbrack \varphi(x,z) \land \mathrm{lh}(\ulcorner \psi\lbrack v_0 \rbrack \urcorner, z) \rbrack \rbrackであることは明らか．
4. 2と3より題意は満たされる．
proof 2:
対角線補題を使わずに，直接的に$ \psi\lbrack x \rbrackを得ることも出来る
1. 論理式$ \alpha(a,b) \equiv \forall_c.\lbrack c = \overline{4} \times b \to \varphi(a,c) \rbrackとし，この論理式の長さを$ lとする．
2. $ \psi\lbrack v_0 \rbrack \equiv \alpha(v_0, \overline{l})とする．
3. ところで，任意の$ n \in \Nに対し，数項の長さ$ | \overline{n} |は$ 3n + 1である．
example: $ \overline{2} \equiv S(S(0))より$ |\overline{2}| = 7
4. $ \psi\lbrack v_0 \rbrackがどうなっているかを展開するとこうなる
$ \psi\lbrack v_0 \rbrack \equiv \forall_z.\lbrack z = 4 \times \overline{\left| \forall_z.\lbrack c = \overline{4} \times b \to \varphi(a,c) \rbrack \right|} \to \varphi(v_0,z) \rbrack
$ lの長さを持つ論理式の一箇所を，$ lの数項に置き換えた論理式が$ \psi\lbrack v_0 \rbrackである．
5. だから$ \psi\lbrack v_0 \rbrackの長さは，$ l - 1 + |\overline{l}| = l - 1 + 3l+1 = 4lである．
$ | \psi\lbrack v_0 \rbrack | = 4l．
6. こうして得られた$ \psi\lbrack v_0 \rbrackが$ T \vdash \forall_x. \left\lbrack \psi(x) \leftrightarrow \varphi(x,| \psi\lbrack v_0 \rbrack |) \right\rbrackを満たすことは明らか．
remark:要するに論理式の長さによって自己言及している．
Notation:
$ \nu(\ulcorner \varphi \lbrack v_0 \rbrack \urcorner, n)は，文$ \varphi(\overline{n}) \land \forall_{v_0,v_1}.\lbrack \varphi(v_0) \land \varphi(v_1) \to v_0 = v_1 \rbrackのGödel数を表すとする．
remark:「$ \varphiが$ nを名乗っている」ということを表している
論理式$ P(x,y)は$ |E_x| \leq yという原始再帰的な関係を表現する$ \Sigma_1論理式とする．
論理式$ Q(x,y) \equiv \exists_z.\lbrack \mathrm{Pr}_T(\nu(z,x)) \land P(z,y) \rbrackとする．
$ \mathrm{Pr}_T(\nu(z,x))と$ P(z,y)は$ \Sigma_1論理式なので，$ Qも$ \Sigma_1論理式である．
「$ xを名乗る，長さが$ y以下の論理式$ E_zが存在する」ことを表す．
論理式$ R(x,y) \equiv \lnot Q(x,y) \land \forall_{z<x}.Q(z,y)とする．
$ \forall_{z<x}.Q(z,y)の部分も$ \Sigma_1である．
「$ xは，長さが$ y以下の論理式では名乗ることも出来ない数である」ことを表す．
Definition:
Lem3.2に$ Rを適用して得られる論理式を$ \xi\lbrack v_0 \rbrackとする．
すなわちこうなる．
$ T \vdash \forall_x. \left\lbrack \xi(x) \leftrightarrow R(x,\overline{|\xi\lbrack v_0 \rbrack |}) \right\rbrack
更に，$ e = | \xi\lbrack v_0 \rbrack |とする．
remark:
1. 算術の言語は有限個しかないから，$ e以下の長さの論理式というのも有限個しかない．
2. 論理式が名乗ることが出来る数は高々1個しか存在しない
3. 1と2より，$ e以下の長さの論理式で名乗ることの出来る数も，当然有限個しか存在しない．
4. $ e以下の長さのどんな論理式でも名乗ることが出来ない数のうち最小の数を$ m_eとする．
このとき，
$ \mathcal{N} \vDash \lnot Q(\overline{m_e}, \overline{e})
$ \mathcal{N} \vDash \forall_{z < \overline{m_e}} Q(z, \overline{e})．さらにこの文は$ \Sigma_1文でもある．
Thm 3.3: 第1不完全性定理, Boolos-Kikuchiの不完全性定理
1. $ Tが無矛盾なら$ T \nvdash \xi(\overline{m_e})
2. $ Tが$ \Sigma_1健全なら$ T \nvdash \lnot\xi(\overline{m_e})
proof:
1について．
1. 背理法で示す．$ T \vdash \xi(\overline{m_e})とする．
2. $ \xiの定義より$ T \vdash \forall_x.R(x,| \xi\lbrack v_0 \rbrack |)となる．
3. 2と$ eの定義より$ T \vdash R(\overline{m_e},e)
4. $ Rの定義より，$ T \vdash \lnot Q(\overline{m_e},\overline{e})である．
3. $ T \vdash Q(\overline{m_e},\overline{e})である．
3.1 2と$ Rの定義より$ T \vdash \forall_{z<\overline{m_e}}.Q(z,\overline{e})
3.2 3.1と
3.1.$ Rの定義より，$ T \vdash \xi(\overline{m_e}) \land \forall_{v_0,v_1}.\lbrack \xi(v_0) \land \xi(v_1) \to v_0 = v_1 \rbrackである．
SnO2WMaN.icon TODO
3.2. 3.1と$ \nuの定義より，$ T \vdash \nu(\ulcorner \xi\lbrack v_0 \rbrack \urcorner,\overline{m_e})．
3.3. 3.2と導出可能性条件D1より，$ T \vdash \mathrm{Pr}_T (\nu(\ulcorner \xi\lbrack v_0 \rbrack \urcorner,\overline{m_e}))．
3.4. 明らかに定義より，$ \mathcal{N} \vDash P(\ulcorner \xi\lbrack v_0 \rbrack \urcorner, \overline{e})である．
3.5. 3.4と$ Tの$ \Sigma_1完全性より，$ T \vdash P(\ulcorner \xi\lbrack v_0 \rbrack \urcorner, \overline{e})
3.6. 3.3と3.5とより，$ T \vdash \exists_z.\lbrack \mathrm{Pr}_T(\nu(z, \overline{m_e})) \land P(z,\overline{e}) \rbrack
ところで$ \exists_z.\lbrack \mathrm{Pr}_T(\nu(z, \overline{m_e})) \land P(z,\overline{e}) \rbrackとは$ Q(\overline{m_e},\overline{e})である．
5. 3と4より$ Tは矛盾する．
6. しかし，$ Tは無矛盾と前提したので議論が破綻する．
7. したがって$ T \nvdash \xi(\overline{m_e})ではない．❏
2について．
1. 背理法で示す．$ T \vdash \lnot\xi(\overline{m_e})とする．
2. $ \xiの定義などより，$ T \vdash \lnot R(\overline{m_e}, e)であり，更に$ T \vdash \forall_{z<x}.Q(z,\overline{e}) \to Q(\overline{m_e},\overline{e})
$ \lnot R(\overline{m_e}, e) \equiv \lnot\lnot Q(\overline{m_e},\overline{e}) \lor \lnot\forall_{z<\overline{m_e}}.Q(z,\overline{e}) \equiv \forall_{z<\overline{m_e}}.Q(z,\overline{e}) \to Q(\overline{m_e},\overline{e})
3. 上のRemarkより，$ \mathcal{N} \vDash \forall_{z < \overline{m_e}} Q(z, \overline{e})であり$ \Sigma_1文
4. 3と仮定の$ \Sigma_1健全性より，$ T \vdash \forall_{z<\overline{m_e}}.Q(z,\overline{e})
5. 2と4より$ T \vdash Q(\overline{m_e},\overline{e})．
6. $ Q(\overline{m_e},\overline{e})は$ \Sigma_1文であるので，$ \Sigma_1完全性より$ \mathcal{N} \vDash Q(\overline{m_e},\overline{e})．
M. Kikuchi, T. Kurahashi, H. Sakai, "On proofs of the incompleteness theorems based on Berry's paradox by Vopěnka, Chaitin, Boolos"#64c70c0f13a158000005440b
7. しかし上のRemarkより$ \mathcal{N} \vDash \lnot Q(\overline{m_e},\overline{e})である．
8. 6と7より$ T \vdash \lnot\xi(\overline{m_e})とすることは出来ないことが明らかとなった．
SnO2WMaN.iconここで意味論的にありえないから仮定が誤っているとした
すなわち$ Tの無矛盾性には訴えていない．
$ \lnot Q(\overline{m_e},\overline{e})は$ \Sigma_1文ではない（$ \Pi_1文である）から
7で$ \mathcal{N} \vDash \lnot Q(\overline{m_e},\overline{e}) \implies T \vdash \lnot Q(\overline{m_e},\overline{e})は帰結しない筈
Cor 3.4
Kikuchi1994のThm 2.2
1. $ Tが無矛盾なら$ T \nvdash \lnot Q(\overline{m_e}, e)
2. $ Tが$ \Sigma_1健全なら$ T \nvdash Q(\overline{m_e}, e)
proof:
Thm 3.3の証明参照．
Remark
$ k \in \Nについて$ n_kを$ v_0,\dots,v_{k-1}を自由変数として含む長さ$ k以下の論理式の個数を表すとする．
Lem 3.5
任意の$ k \in \Nについて，
$ T \vdash \mathrm{Con}_T \to \exists_{z \leq \overline{n_k}}.\lnot Q(z,\overline{k})
proof:
1. $ Qの定義より，
$ T + \forall_{z<\overline{n_k}}.Q(z,\overline{k}) \vdash \exists_{x_0,\dots,x_{n_k}}.\lbrack \mathrm{Pr}_T(\nu(x_0,\overline{0})) \land \cdots \land \mathrm{Pr}_T(\nu(x_{n_k},\overline{k})) \land P(x_0,\overline{k}) \land \cdots \land P(x_{n_k},\overline{k}) \rbrack
2. 鳩の巣原理より以下を満たす相異な$ i,j \leq n_kが存在する．
$ T + \forall_{z<\overline{n_k}}.Q(z,\overline{k}) \vdash \exists_{x_i}.\lbrack \mathrm{Pr}_T(\nu(x_i,\overline{i})) \land \mathrm{Pr}_T(\nu(x_i,\overline{j})) \rbrack
3. $ \mathrm{Pr}_T(x)については以下の性質が成り立つ．
$ T \vdash \forall_x.\lbrack \mathrm{Pr}_T(\nu(x_i,\overline{i})) \land \mathrm{Pr}_T(\nu(x_i,\overline{j})) \rbrack \to \mathrm{Pr}_T(\ulcorner \overline{i} = \overline{j} \urcorner)
4. 2と3より，$ T + \forall_{z<\overline{n_k}}.Q(z,\overline{e}) \vdash \mathrm{Pr}_T(\ulcorner \overline{i} = \overline{j} \urcorner)
5. 自明な事実として，相異な$ i,jに対しては$ T \vdash \mathrm{Con}_T \to \lnot\mathrm{Pr}_T(\ulcorner \overline{i} = \overline{j} \urcorner)
6. 4と5より，$ T + \forall_{z<\overline{n_k}}.Q(z,\overline{k}) + \mathrm{Con}_Tは矛盾する．
7. 演繹定理より$ T \vdash \mathrm{Con}_T \to \exists_{z<\overline{n_k}}.\lnot Q(z,\overline{k})．❏
$ T + \mathrm{Con}_T \vdash \lnot\forall_{z<\overline{n_k}}.Q(z,\overline{k})
$ T + \mathrm{Con}_T \vdash \exists_{z<\overline{n_k}}.\lnot Q(z,\overline{k})
$ T \vdash \mathrm{Con}_T \to \exists_{z<\overline{n_k}}.\lnot Q(z,\overline{k})
remark
より詳細はKikuchi1994のLem 3.3を参照．
Lem 3.6
任意の$ m \in \Nについて，
$ T + \forall_{z \leq \overline{m}}.Q(z,\overline{e})が矛盾するなら，$ T + \forall_{z < \overline{m}}.Q(z,\overline{e})も矛盾する．
remark:わかりづらすぎるが，前提は$ z \leq \overline{m}，結論は$ z < \overline{m}．
proof: #TODO
1. $ T + \forall_{z \leq \overline{m}}.Q(z,\overline{e})が矛盾すると仮定する．
2. $ T + \forall_{z < \overline{m}}.Q(z,\overline{e}) \vdash \xi(\overline{m})
$ T + \forall_{z < \overline{m}}.Q(z,\overline{e}) \vdash \lnot Q(\overline{m},\overline{e}) \land \forall_{z < m}.Q(z,\overline{e})
$ \leq, <の違いに注意
SnO2WMaN.icon?
$ Rの定義より$ R(\overline{m},\overline{e}) \equiv \lnot Q(\overline{m},\overline{e}) \land \forall_{z < m}.Q(z,\overline{e})
$ \xiの定義より$ T \vdash \xi(\overline{m}) \leftrightarrow R(\overline{m},\overline{e})
3. $ T + \forall_{z < \overline{m}}.Q(z,\overline{e}) \vdash \xi(\overline{m}) \land \forall_{v_0,v_1}.\lbrack \xi(v_0) \land \xi(v_1) \to v_0 = v_1 \rbrack
4. $ T \vdash \forall_{z < \overline{m}}.Q(z,\overline{e}) \to (\xi(\overline{m}) \land \forall_{v_0,v_1}.\lbrack \xi(v_0) \land \xi(v_1) \to v_0 = v_1 \rbrack)
5. $ \forall_{z < \overline{m}}.Q(z,\overline{e})は$ \Sigma_1文である
6. 導出可能性条件と5より$ T \vdash \mathrm{Pr}_T(\ulcorner \forall_{z < \overline{m}}.Q(z,\overline{e}) \urcorner) \to \mathrm{Pr}_T(\nu(\ulcorner \xi\lbrack v_0 \rbrack \urcorner, \overline{m}))
7.
一方，
8. $ T \vdash P( \ulcorner \xi\lbrack v_0 \rbrack \urcorner, \overline{e})より$ T \vdash \forall_{z < \overline{m}}.Q(z,\overline{e}) \to Q(\overline{m},\overline{e})
9. 8より$ T + \forall_{z < \overline{m}}.Q(z,\overline{e}) \vdash Q(\overline{m},\overline{e})である．
よって，
10. $ T + \forall_{z < \overline{m}}.Q(z,\overline{e}) が$ Q(\overline{m},\overline{e})と$ \lnot Q(\overline{m},\overline{e})を証明するので，$ T + \forall_{z < \overline{m}}.Q(z,\overline{e}) は矛盾している．
4. $ T + \forall_{z < m}.Q(z,\overline{e}) \vdash \mathrm{Pr}_T(\nu(\ulcorner \xi\lbrack v_0 \rbrack \urcorner, \overline{m}))
5. $ T \vdash \forall_{z < m}.Q(z,\overline{e}) \to \mathrm{Pr}_T(\nu(\ulcorner \xi\lbrack v_0 \rbrack \urcorner, \overline{m}))
Lem 3.7
$ Tが無矛盾なら，任意の$ m \in \Nについて$ T \nvdash \exists_{z \leq \overline{m}}.\lnot Q(z,\overline{e})．
proof: #TODO
$ mについての帰納法．
初期ステップ
Lem 3.6
帰納ステップ
$ T \nvdash \exists_{z \leq \overline{m}}.\lnot Q(z,\overline{e})であると仮定すると$ T \nvdash \exists_{z < \overline{m}}.\lnot Q(z,\overline{e})であることを示す．
$ \leqと$ <に注意．
1. IHより$ T \nvdash \exists_{z \leq \overline{m}}.\lnot Q(z,\overline{e})であるとする．
2. 1より$ T + \exists_{z \leq \overline{m}}.\lnot Q(z,\overline{e})は矛盾する．
3. 2より$ T + \forall_{z \leq \overline{m}}.Q(z,\overline{e})は矛盾する．
$ \exists_{z \leq \overline{m}}.\lnot Q(z,\overline{e}) \equiv \forall_{z \leq \overline{m}}.Q(z,\overline{e})であることに注意する．
4. Lem3.6より$ T + \forall_{z < \overline{m}}.Q(z,\overline{e})は矛盾する．
5. 4より$ T \nvdash \exists_{z < \overline{m}}.\lnot Q(z,\overline{e})
$ T \vdash \exists_{z < \overline{m}}.\lnot Q(z,\overline{e})と仮定する
このとき$ T \vdash \lnot \forall_{z < \overline{m}}. Q(z,\overline{e})であるので$ T + \forall_{z < \overline{m}}. Q(z,\overline{e})は矛盾する．
したがって$ Tは矛盾する．
$ T + \forall_{z \leq \overline{m}}.Q(z,\overline{e})が矛盾するなら，$ T + \forall_{z < \overline{m}}.Q(z,\overline{e})も矛盾する．
Thm 3.8: 第2不完全性定理
$ Tが無矛盾なら，$ T \nvdash \mathrm{Con}_T
proof:
1. $ \mathrm{Con}_Tが証明可能だとするとLem 3.5より$ T \vdash \exists_{z \leq \overline{n_e}}.\lnot Q(z,\overline{e})
2. 他方，$ Tが無矛盾なのでLem3.7より$ T \nvdash \exists_{z \leq \overline{n_e}}.\lnot Q(z,\overline{e})
3. 1と2より破綻する．よって$ \mathrm{Con}_Tは証明可能ではない．❏